es:ES, Cmd, Rsp:Type, isupdate:(Cmd), In:AbsInterface(Cmd), Out:AbsInterface(Rsp),
Delta:(({c:Cmd| (isupdate(c))}  List)Rsp),
Q:(({c:Cmd| (isupdate(c))}  List){c:Cmd| ((isupdate(c)))} Rsp).
approx_sm(es; In; Out; Cmd; isupdate; Rsp; Delta; Q)   

latex

Up	abstract chain replication
Definitions of Statement	approx_sm(es; In; Out; Cmd; isupdate; Rsp; Delta; Q)
Definitions	s = t, t  T, x:AB(x), x:A. B(x), ES, EState(T), a:A fp B(a), f(a), Id, , strong-subtype(A;B), P  Q, Type, EqDecider(T), Unit, left + right, IdLnk, x:A  B(x), EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', , b, constant_function(f;A;B), SWellFounded(R(x;y)), , pred!(e;e'), x,y. t(x;y), !Void(), x:A.B(x), Top, S  T, suptype(S; T), first(e), A, <a, b>, pred(e), x.A(x), x. t(x), P & Q, E, AbsInterface(A), {x:A| B(x)} , approx_sm(es; In; Out; Cmd; isupdate; Rsp; Delta; Q), E(X), X(e), is-query(In;isupdate;e), False, (x  l), X(L), l1  l2, P  Q, null(as), e c e', (e < e'), case b of inl(x) => s(x) | inr(y) => t(y), True, as @ bs, e  X, A c B, ff, tt, rec-case(a) of [] => s | x::y => z.t(x;y;z), let x,y = A in B(x;y), t.1, a < b, x:A. B(x), if b then t else f fi , , Outcome, #$n, A  B, ||as||, l[i], |g|, map(f;as), A List, inr x , inl x , P  Q, P  Q, f(x)?z
Lemmas	map wf, es-interface-val wf, length wf1, select wf, es-causl wf, btrue wf, bfalse wf, null wf, es-is-interface wf, false wf, append wf, true wf, l member wf, es-causle wf, null wf3, iseg wf, is-query wf, es-interface-val wf2, es-interface-vals wf, es-E-interface wf, es-interface wf, es-E wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, assert wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf, event system wf